Step of Proof: assert_of_eq_bool
9,38
postcript
pdf
Inference at
*
1
1
1
I
of proof for Lemma
assert
of
eq
bool
:
1. ff = tt
False
latex
by AssertLemma `btrue_neq_bfalse` []
latex
1
:
1:
2.
(tt = ff)
1:
False
.
Lemmas
btrue
neq
bfalse
origin
False
by AssertLemma `btrue_neq_bfalse` []
1:
1: 2. 
(tt = ff)
1: False
. False
by AssertLemma `btrue_neq_bfalse` []
1:
1: 2. (tt = ff)
1: False
.